(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const r1 Real)
(declare-const r3 Real)
(assert v0)
(assert v1)
(assert v3)
(assert (= (* (/ 271866967.0 50000000.0) r1 9.0 r3) 9.0))
(assert v4)
(check-sat)
